Курс Программирования Если бы я составлял требования для вхождения в мою компанию, я бы конечно ввел обязательным изучения программировния с точки зрения Робертов Милнера и Харпера на примере языка ML. Конечно необходимыми были бы изучения Хаскеля, Эрланга и немного матана. Я сам этого всего не знаю, поэтому этот курс я создаю сам для себя и сам являюсь первым его студентом. Курс 1. Однотипная лямбда Первый обязательный язык программирования был бы Эрланг, который заодно является основным в нашей компании. Сразу после этого шло бы изучение базового курса лямбда исчисления и категориальной абстракной машины. На примере Эрланг был бы описан подход в построения языка с одним типом данных (динамчески-типизированного как счас говорят) а также два вида виртуальных машин регистровой и стековой. Здесь был бы обязательный курс Саймона про построение функционального языка программирования и стековой машины. Тем более что есть хорошие примеры на Хаскеле kivi. * Лямбда исчисление, например по Вольфенхагену или курсу МИФИ2003 * Исчисление процессов по Роберту Милнеру * Эрланг по Джо Армстронгу * Создание функционального языка по Сайомону Пайтону Джонсу Главный инсайт этого курса это открытие комбинаторной логики и формализации вычислений, а также такие вещи как компиляция, виртуальные машины и исчисление процессов на примере Эрланга. Курс 2. Типизированная лямбда После изучения лямбда исчисления и понимания как работает вычислитель в рамках декартово замкнутой категории следующим языком я бы выбрал ML и одновременно и паралеьно Haskell. Сам я сейчас нахожусь на этом уровне и я очень рад что я немного разобрался в предыдущей теме за прошедшие пару лет. Целый год я посвятил языку Эрланг и ни сколько не жалею об этом. Немного я жалею о другом, что я провел больше 10 лет на С/C++/C#/Java. Если этот курс читается человеку, интеллект которого не обезображен объектно-ориентированным программированием я бы преподавал на SML, в противном случае я бы выбрал OCaml для преподавания, что бы была возможность сравнения функционального стиля и объектно-ориентированного при разработке сложных систем и подходов к повторному использованию кода. Главный инсайт этого курса должно стать понимание разницы между категориями, где объекты -- это типы, а морфизмы функции, и категориями, где объекты -- это сигнатуры (типы и функции), а морфизмы - это функторы на сигнатурах. И здесь ML очень наглядно и выразительно это демонстрирует. Правда десять лет назад это было не так очевидно и не так разработано. Начиная с этого места было бы крайне уместно дать основы теории категорий, я думаю, не раньше. Тут можно объяснять и доказывать что катеория для лямбда исчисления это декартово замкнутая категория с умножением и степенью. Дальше следовало бы показать что категория модулей ML сигнатур и функторов это по сути 2-категория над категорией типов и функций. Здесь расказать об индексированных категориях, пучках Гротендика и т.д. и заодно доказать что эта 2-категория тоже является декартово замкнутой, и, таким образом реализует лямбда исчисление находящееся на другом уровне. Здесь уже можно начать рассказывать о System F и лямбда кубе. Надо сказать что уровень на котором находится сейчас ML и Хаскель недостаточен для плавного перехода на каждый следующий уровень абстракции поэтому ведутся попытки унификации языков программирования что бы n-категории которые появляются на каждом шаге плавно выводились из предыдущего уровня с унифицированым синтаксисом, и не так сильно обрубывался (как это можно видеть в Haskell->Agda, OCaml->Coq) переход к исчислению конструкций которое должно стать потолком этого второго курса. Обязательным для ознакомления здесь были бы все языки которые призваны решить эту проблему языковой унификации при переходе от однотипной лямбды к к исчислению конструкций. Дальше было бы полезно расказать о святой троицы вычислений Карри-Говарда: Логика, которая присваивает первенство доказательствам и пропозициям; Языки, которые считают первичными программы и типы; Категории, которые считают первичными отображения и структуры; -- которая является божественным проявлением одной сущсности. * ML по Роберту Харперу и Хаскель паралельно * Основы теории категорий * Computational Category Theory с примерами на ML * Категориальный ЯП на диалгебрах от Хагино * Категориальное обоснование системы модулей ML * Изоморфизм Карри-Говарда, Agda или Coq по выбору, исчисление конструкций Решил даже сделать аннотированную библиотеку http://spawnproc.com/ с хинтами как читать книжки в каком порядке. _____________ http://synrc.com/publications/cat/